E,X1,X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), info:(E((:Id  X1) + (:(:IdLnk  E)  X2))),
e,r:E, l:IdLnk.
(rcv-from-on(dE; dL; info; e; l; r))  ((rcv?(r)) c ((sender(r) = e)  (link(r) = l))) 

latex

Definitions	x:A. B(x), b, rcv-from-on(dE; dL; info; e; l; r), band(p; q), t  T, P  Q, tt, if b then t else f fi , ff, prop{i:l}, P  Q, A c B, True, P  Q, P  Q, , Unit,
Lemmas	rcv? wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, IdLnk wf, Id wf, deq wf, iff functionality wrt iff, band wf, sender wf, link wf, assert of band, and functionality wrt iff, deq property